package sketch.specs;

import java.io.File;
import java.io.IOException;
import java.util.LinkedHashSet;
import java.util.Set;

import org.eclipse.jdt.core.dom.MethodDeclaration;
import org.eclipse.jdt.core.dom.TypeDeclaration;

import randoop.util.Files;
import sketch.ast.ASTUtils;
import sketch.util.Checker;
import sketch.util.Globals;

public class WriteJPFSymbolicTestDriver {
	
	//should also add imports
	public static void writeTestDriver(TypeDeclaration type, String dir, String[] methodsUnderTest) {
		MethodDeclaration[] declarations = type.getMethods();
		Set<String> methodSet = new LinkedHashSet<String>();
		for(String methodUnderTest : methodsUnderTest) {
			methodSet.add(methodUnderTest);
		}
		//process every method
		for(MethodDeclaration declaration : declarations) {
			String methodName = declaration.getName().getIdentifier();
			if(!methodSet.contains(methodName)) {
				continue;
			}
			//check the modifiers
			Checker.checkTrue(declaration.parameters().isEmpty(), "The parameter of method: " + methodName + " is not empty!");
			Checker.checkTrue(ASTUtils.isPublic(declaration), "The given method should be public!");
			Checker.checkTrue(declaration.getReturnType2().toString().equals("void"), "The return type of method: " + methodName + " is not void.");
			
			String singleDriverName = type.getName().getIdentifier() + "_" + methodName;
			String singleFilePath = dir + Globals.fileSep +  singleDriverName + ".java";
			writeSingleDriver(singleFilePath, singleDriverName, type.getName().getIdentifier(), methodName);
		}
	}
	
	static void writeSingleDriver(String filePath, String driverName, String testClassName, String methodName) {
		File file = new File(filePath);
		StringBuilder sb = new StringBuilder();
		
		//set the file content
		sb.append("import gov.nasa.jpf.symbc.Debug;");
		sb.append(Globals.lineSep);
		
		sb.append("public class " + driverName + " {");
		sb.append(Globals.lineSep);
		sb.append("  public static void main(String[] args) {" + Globals.lineSep);
		sb.append("    " + testClassName + " c = new " + testClassName + "();" + Globals.lineSep);
		sb.append("    c." + methodName + "();" + Globals.lineSep);
		sb.append("    Debug.printPC(\"" + driverName + " Path Condition: \");" + Globals.lineSep);
		sb.append("  }" + Globals.lineSep);
		sb.append("}" + Globals.lineSep);
		
		//write to the file
		try {
			Files.writeToFile(sb.toString(), file);
		} catch (IOException e) {
			throw new RuntimeException(e);
		}
	}
	
}